f-newround{$x:ut2, $free:ut2, $mine:ut2}
f-newround(es; L; e)
== ((loc(e)  L)  @e(mkid{$x:ut2}mkid{$free:ut2}))
==  (es-when(es; mkid{$x:ut2}; e) = mkid{$mine:ut2}) 

latex

---

clarification:

f-newround{$x:ut2, $free:ut2, $mine:ut2}
f-newround(es; L; e)
== ((es-loc(es; e)  L  Id)  es-change-to(es;Id;mkid{$x:ut2};e;mkid{$free:ut2}))
==  (es-when(es; mkid{$x:ut2}; e) = mkid{$mine:ut2}  Id) 

latex

Definitions	P  Q, (x  l), loc(e), @e(xv), s = t, Id, es-when(es; x; e), mkid{$x:ut2}
FDL editor aliases	f-newround